
(* Programme de test auto *)

open Format
open Lexing
open Lexer
open Parser
open Ast
open Cub
open Atom
open Compile

let mk_node e t = {data = t; node = e}
let loc_dummy e =
  mk_node e (Lexing.dummy_pos, Lexing.dummy_pos)





(***  testing on the dnf transformation function  ***)
    
let create_var s =
  mk_node (LTterm (      
    mk_node ( TMatom (
      mk_node ( ATleftval (
        mk_node ( LVident (loc_dummy s)) Tany)
      ) Tany
    )) Tany
  )) Tany

let create_set_var s = Comp (Elem s, Eq, Elem "True")
    
let x = create_var "x" 
let y = create_var "y" 
let z = create_var "z" 
let w = create_var "w" 

let (|||) lt1 lt2 = mk_node (LTop (Bor, lt1, lt2)) Tany
let (&&&) lt1 lt2 = mk_node (LTop (Band, lt1, lt2)) Tany
  
let create_satom s1 s2 =
    SAtom.add (create_set_var s2)
      (SAtom.singleton (create_set_var s1))
  
  
let fmla1 = (x ||| y) &&& (w ||| z)

let print_dnf dnf =
  SSAtom.iter (fun satom ->
    print_satom true Format.std_formatter satom;
    printf "\n||@\n"
  ) dnf

let () =
  let ssres = SSAtom.singleton (create_satom "x" "w") in
  let ssres = SSAtom.add (create_satom "x" "z") ssres in
  let ssres = SSAtom.add (create_satom "y" "w") ssres in
  let ssres = SSAtom.add (create_satom "y" "z") ssres in
  let ss = purednf fmla1 in
  if ss = ssres then printf "dnf : SUCCESS@."
  else printf "dnf : FAIL@."
  
    
    
  
    
(***      non-regression tests : test directory     ***)

let current_test_file = ref ""
  
let rec iter_dir f dir =
  let filenames = Sys.readdir dir in
  Array.iter (fun e ->
    let rel = dir ^ Filename.dir_sep ^ e in
    current_test_file := rel;
    if Sys.is_directory rel then iter_dir f rel
    else if (Filename.check_suffix rel ".any") && not ((rel.[0]) = '.')
    then f rel
  ) filenames

let ok_disp = "SUCCESS"
let fail_disp = "FAIL"

let parsing_fail f = 
  let c = open_in f in
  let lb = Lexing.from_channel c in
  try 
    let _p = Parser.prog Lexer.token lb in
    eprintf "%s : \t%s\n" f fail_disp
  with _ -> printf "%s : \t%s\n" f ok_disp;
  close_in c


let parsing f = 
  let c = open_in f in
  let lb = Lexing.from_channel c in
  let p = Parser.prog Lexer.token lb in
  p

let parsing_success f = try ignore (parsing f); printf "%s : \t%s\n" f ok_disp
  with _ -> eprintf "%s : \t%s\n" f fail_disp
    

let typing_fail f =
  Typing.clear_envs ();
  let p = parsing f in
  try ignore (Typing.type_prog p); eprintf "%s : \t%s\n" f fail_disp
  with _ -> printf "%s : \t%s\n" f ok_disp

    
let typing_success f =
  Typing.clear_envs ();
  let p = parsing f in
  try ignore (Typing.type_prog p); printf "%s : \t%s\n" f ok_disp
  with e ->
    eprintf "%s : \t%s\n" f fail_disp;
    eprintf "%s\n" (Printexc.to_string e)

let () =
  try
    iter_dir parsing_fail "test/fail/parsing";
    iter_dir typing_fail "test/fail/typing";
    iter_dir parsing_success "test/success/parsing";
    iter_dir typing_success "test/success/typing";
  with
  | Lexical_error _ as e ->
      eprintf "%s : \n" !current_test_file;
      eprintf "Lexical error : %s\n@." (Printexc.to_string e);
      exit 1
  | Typing.Error _ as e ->
      eprintf "%s : \n" !current_test_file;
      eprintf "Typing : %s\n@." (Printexc.to_string e);
      exit 1;
  | Parsing.Parse_error as e->
      eprintf "%s : \n" !current_test_file;
      eprintf "Parsing: %s\n@." (Printexc.to_string e);
      exit 1
  | e ->
      eprintf "%s : \n" !current_test_file;
      eprintf "Anomaly: %s\n@." (Printexc.to_string e);
      exit 1
